Programming languages for trustworthy AI systems
Zhong Shao's primary research interests encompass programming languages, formal methods, operating systems, and computer security. Within these fields, he is a strong proponent of certified software and firmly believes that certified programming, accompanied by formal proofs, presents the most promising approach to constructing truly reliable software and effectively managing the increasing complexity of future AI systems. In his laboratory, Shao and his team have recently dedicated their efforts to constructing cyber-physical systems that boast robust security guarantees, including self-driving cars and crewless ground/aerial vehicles. Additionally, they have explored real-time machine learning for embedded systems and delved into the realm of the Internet of Things. Notably, their work focuses on system design, algorithmic techniques, and formal methods aimed at constructing secure, dependable, and accountable AI systems.
Methods
Topics
Biography
Shao is the Thomas L. Kempner Professor of Computer Science at Yale University. He earned his PhD in Computer Science from Princeton University and joined Yale as a faculty member in 1994. During the last 30 years, Shao and his team at Yale have led and pioneered work on language-based approaches to safety and security, certified OS kernels, certified compilation, and formal methods. His work on CertiKOS is widely considered a breakthrough toward building hacker-resistant operating systems that are provably free from cyber vulnerabilities. Shao is also a co-founder of the blockchain security startup CertiK.